ErasedMacro4.agda:19,1-19
Variable A is declared erased, so it cannot be used here
when checking that the expression A has type Set
